perm filename MRS.INF[MRS,LSP]1 blob
sn#577625 filedate 1981-09-30 generic text, type T, neo UTF8
~(635)\f5b
STANFORD HEURISTIC PROGRAMMING PROJECT December 1980
Memo HPP-80-24~j\f5 1f0 7f5 2f0 8f5 2f0 10f5 2f0 6f5
MRS Manual~c\f5 2f0 10f5b
by~c\f5b
Michael R. Genesereth, Russell Greiner, and David Smith
DEPARTMENT OF COMPUTER SCIENCE
School of Humanities and Sciences
STANFORD UNIVERSITY ~c\f5b56B
~j\f5
Table of Contents~ck792\f5 1i
1. Introduction~j\i
2. Informal Description of MRS~j\i
2.1 The Language
2.2 Storage and Retrieval
2.3. Inference
2.4 Theories (i.e. Contexts)
2.5 Meta-Description
2.6 Advice-Taking and Explanation
Example - Changing the Inference Algorithm
Example - Changing the Representation
Example - Procedural Attachment
Example - Truth Maintenance
2.7 Meta-Control
2.8 Complete Modifiability
3. Subroutines and Variables
3.1 User-Level Subroutines
3.2 Predefined Inference Methods
3.3 Semantic Network Subroutines
3.4 Data Structure Manipulation Routines~j\i404I1i29I1i35I1i35I1i
4. The Syntax of MRS
4.1 First Order Propositions
4.2 Higher Order Propositions
4.3 Meta-Level Propositions~j\i
5. Initial Vocabulary
5.1 Logic
5.2 Sets and Mappings
5.3 Arithmetic
5.4 Events and Time
5.5 Meta-Level Vocabulary~j\i1I1i24I1i12I1i24I1i17I1i22I1i
6. Initial Data Base
6.1 Definitions of the User-Level Subroutines
6.2 Meta-Assertions
7. Using MRS
7.1 System Utilities
7.2 MRS in Maclisp
7.3 MRS in Interlisp~j\i1I1i23I1i48I1i36I1i23I1i21I1i
References~e12j\i
Appendix - META Module~e12j\i
Appendix - LOGIC Module~e12j\i
Appendix - DEMON Module~e12j\i
Appendix - OPERATIONS Module~e12j\i
1. Introduction~jk792\i
MRS is a knowledge representation system intended for use by AI researchers in building expert systems. It offers a diverse repertory of commands for asserting and retrieving information, with varying degrees of inference. Information is entered in a predicate calculus-like language of assertions and is stored in either a propositional network or any of a variety of specialized data representations (e.g. property lists, alists, bit vectors). The initial system includes a vocabulary of concepts and facts about logic, sets, mappings, arithmetic, and procedures.~j
What makes MRS special among knowledge representation systems is its ability to deal with itself in the same way that it deals with application domains (like geology and medicine). In MRS, the basic representation is described within the representation itself, and the inference techniques used in reasoning about application domains can be applied to reasoning about the system. For example, MRS might use facts about sets and sequences to determine whether a statement is provable, or it might use facts about directed graphs to determine that backward chaining is the most appropriate technique to use with forward branching search spaces.~j
Furthermore, MRS is fully modifiable in that it can be converted into any LISP program by making assertions within its own formalism (hence the name "Modifiable Representation System"). Most knowledge representation systems were developed in the context of particular applications, e.g. KRL and OWL in natural language and Units in molecular biology. The problem is that what is good for one application is usually not perfect for another. Although most systems offer their users a number of options, there are often undesirable design decisions that cannot be changed. In MRS modifiability is a design goal. Of course, bare LISP is similarly modifiable, but MRS is special in the extent to which it facilitates the transformation to other interesting knowledge representation system behaviors. With a few statements, it is possible to select a new data structure (e.g. property lists) or enable a different inference algorithm (e.g. inheritance over a "parts" hierarchy). The facility is due to MRS's structure and the explicit knowledge about knowledge representation encoded within it.~j\77f1 3f0 553f1 3f0
Section 2 of this manual provides an informal overview of the system, and section 3 lists the system's subroutines and variables. Section 4 describes the syntax of the representation in detail; section 5 presents the initial vocabulary; and section 6 lists the initial data base of facts about its predefined symbols. A summary of the system's utilities and the details of loading and using MRS are given in section 7.~j
Honesty: At present, MRS's capabilities are fairly rudimentary. The strength of the system at this point lies more in its clean formalism and powerful architecture than in practical deductive capabilities. However, it is certainly no less capable than any other knowledge representation system, and the development of the system's knowledge about knowledge representation and the implementation of effective self-control capabilities are tasks of high priority for the authors. ~j\1i479I
2. Informal Description of MRS~j\i
This section provides an informal overview of MRS. Note that it is not a primer or introduction to the idea of self-descriptive, self-controlling, modifiable knowledge representation systems; it is merely a recapitulation of MRS's features and terminology for those already familiar with the idea. (For a discussion of the theory underlying MRS, the reader should consult [Genesereth & Lenat]).
2.1 Syntax~j\400i10I
The syntax of the predicate calculus-like language is straightforward and should be apparent from some examples. Each symbol in an assertion is either a variable or a constant and can stand for an object, a function, an action, a relation, a relation on relations, a relation on actions, etc. Each complete lists makes up a formula. The examples in figure 1 show how the various types of formulas in first order predicate calculus are expressed. Atomic formulas are represented by grouping symbols together with a relation symbol of the appropriate type. Non-atomic formulas are expressed by relating several formulas with a logical symbol.~j
Bertram and Arthur are neighbors.
(Neighbor Bertram Arthur)
Carleton is not Bertram's neighbor.
(Not (Neighbor Carleton Bertram))
Either Carleton is Bertram's father or Beatrice is his mother.
(Or (Father-of Carleton Bertram) (Mother-of Carleton Beatrice))
All apples are red.
(All x (If (Mem x Apples) (Color-of x Red)))
Some apple is green.
(Some x (And (Mem x Apple) (Color-of x Green)))
Everybody has someone he loves.
(All x (Some y (Loves x y)))
There is someone whom everybody loves.
(Some y (All x (Loves x y)))~j\b3B36b26B1b2B38b33B66b68B21b47B24b50B35b31B42b
Figure 1 - First Order Predicate Calculus~c\1b41B
Higher order formulas are formed either by using functional or relational variables or by applying higher order relations to functional or relational constants. The induction axiom shown in figure 2 is a simple example. (Note that asserting such facts does not necessarily ensure that they will be used. Whether an axiom is used or not depends on the inference procedure the user has selected.)~j\225b173B
Whenever 0 is in a set and n's membership in the set implies the
membership of n+1, then all integers are in the set.
(all s (if (and (s 0) (all n (if (s n) (s (+ n 1)))))
(all n (s n))))~j\123b2B1b
Figure 2 - An Example of a Second Order Formula~c\1b47B
Two useful syntactic features are illustrated in figure 3. The first is the use of the prefix characters $ and ? to denote universal variables and existential variables without universals quantified to their left. Second, a function in MRS can be used in two ways, either with its arguments in places reserved for individuals or in assertions with its value as the last argument.~j\108b1B5b1B
Every neighbor of Bertram is a neighbor of Beatrice.
(all x (if (neighbor x Bertram) (neighbor x Beatrice)))
(if (neighbor $x Bertram) (neighbor $x Beatrice))
Some apple is green.
(some x (and (mem x apple) (color-of x green)))
(and (mem ?x apple) (color-of ?x green))
Beatrice is Carleton's mother.
(mother-of Carleton Beatrice)
(= (mother-of Carleton) Beatrice)~j\57b59B3b54B24b47B4b40B39b
Figure 3 - Some abbreviations~c\b30B
2.2 Storage and Retrieval~j\i
In MRS there is a distinction between the language a person uses in expressing information and the representation the system uses in storing it. Figure 4 presents the situation graphically. All information is entered in a predicate calculus-like language of assertions and is stored in a variety of representations. For example, the values of unary functions can be stored on property lists, procedures can be stored as LISP lambda expressions or compiled code, and finite feature sets can be represented as bit vectors. The user can select the representation that he thinks most appropriate, or he can tailor a representation to his particular application. Where no specialized data structure is indicated, MRS simply stores assertions in its propositional net. This multiplicity of representations is essential in making MRS fully modifiable, as discussed in [Genesereth & Lenat]. The advantages and problems are discussed more fully in [Genesereth].~j\426f1 3f0
Predicate
Calculus
|
-------------------------------------------------------------------------------
| | | |
Plists Compiled Code Bit Vectors Propositional Net~j
Figure 4 - Language vs. Representation~c\1b
Propositions can be stored and removed from MRS's data base using the subroutines stash and unstash. The lookup subroutine checks whether a proposition is in the data base and returns ((t . t)) if succesful and nil otherwise. If the proposition contains existential variables, lookup returns a binding list for those variables. Lookups (the plural) returns a list of all bindings for which there is a proposition in the data base. Consider the following examples. ~j\84b5B5b7B7b6B73b9B18b3B64b6B46b7B
(stash '(neighbor Arthur Bertram))
(neighbor Arthur Bertram)
(stash '(neighbor Arthur Billings))
(neighbor Arthur Billings)
(lookup '(neighbor Arthur Billings))
((t . t))
(lookup '(neighbor Arthur ?x)) or (lookup '(exist ?x (neighbor Arthur ?x)))
((?x . Bertram) (t . t))
(lookups '(neighbor Arthur ?x))
(((?x . Bertram) (t . t)) ((?x . Billings) (t . t)))
(unstash '(neighbor Arthur Billings))
(neighbor Arthur Billings)
(lookup '(neighbor Arthur Billings))
nil
(lookups '(neighbor Arthur ?x))
(((?x . Bertram) (t . t)))~l4269j\1b204B4b324B
Stash, unstash, and lookup all do inference at the meta-level to determine which representation to use in processing their arguments, but they do no inference on the propositions themselves. The choice of representation can be constrained by the user, as explained above and in section 2.6.~j\2b5B2b7B6b6B
2.3 Inference~j\2i13I
As a convenience for its users, MRS offers a limited amount of automatic inference. Whenever a fact is asserted, the system may infer other facts and assert them as well. Whenever a user asks MRS whether a fact is true, the system may be able to deduce it even though the fact is not explicitly stored. The subroutines assert, unassert, truep, and trueps all perform inference in processing their arguments. Consider the following examples.~j\i2I322b6B2b8B2b5B6b6B87b
(assert '(elephant clyde))
(elephant clyde)
(assert '(if (elephant $x) (color-of $x grey)))
(if (elephant $x) (color-of $x grey))
(truep '(color-of clyde ?y))
((?y . grey) (t . t))~l4269j\b183B
The system's default inference method for retrieving information is depth-first backward chaining. However, a number of other inference methods are defined as well, and the user can instruct MRS to use any one of these or one of his own. This includes the ability to specify different techniques for different types of assertions, e.g. the user may specify direct lookup for mother-of information and property inheritance for color-of information. In the initial system, no inference is done when the user makes assertions. In order to enable such inferences, the user should consult section 2.6.~j\379b9B42b8B
The ultimate goal of MRS's designers is to provide a system with extensive knowledge about inference methods and search control. The current system is only a start in that direction and may not provide all the control capabilities required by a particular application. However, this is not a fault of the representation. The formalism and semantics are completely general and were designed only after careful consideration of numerous representational issues. Thus, even when the built-in inference methods are inadequate and the user is forced to write his own, he should retain the representation and semantics described here.~j
2.4 Theories (i.e. Contexts)~j\2i
There are a number of subroutines and variables in MRS that make it possible for a user to bind together a set of assertions into a named theory. Once this is done, the user can have MRS assume or forget all of the assertions in the set merely by activating or deactivating their theory. Any atom can be the name of a theory, and the assertions contained in that theory will be retained in storage until the user destroys them individually by using unassert or destroys them as a whole by using ut-kill to eliminate the theory to which they belong.~j\140i6I307b8B38b7B
Theories form a partial order, with a single root called global. When a theory is "active", all of the assertions in that theory are available for use in deductions and retrievals, as are all the facts in any theory which is subordinate to it in the partial order. When a theory is "inactive", its assertions are not available unless they are also contained in some other theory and that theory is active. Global is always active, and in a fresh MRS, it is the only known theory.~j\59b6B346b6B
In order to activate a theory, one uses the command ut-Activate. To deactivate a theory, the command is ut-Deactivate. The variable ActiveTheories is a list of all currently active theories. In order to make one theory a subtheory of another in the partial order, one merely asserts a subtheory relationship between them.~j\54b11B42b13B16b14B140b9B
Whenever a user makes a new assertion, it is placed in the context named as the value of the variable CurrentTheory. Similarly, Unassert references the current value of CurrentTheory. To change theories, one simply rebinds CurrentTheory to the desired theory. The value of CurrentTheory is automatically "active" in the sense described above. In order to change an assertion from one theory to another, one simply unasserts its old MyTheory property and asserts the new one.~j\104b13B14b8B33b13B42b13B38b13B147b8B
As an example of theories in MRS, consider the interaction below.~j
(setq CurrentTheory 'earth)
earth
(assert '(color-of sky blue))
(color-of sky blue)
(setq CurrentTheory 'mars)
mars
(truep '(color-of sky ?y))
nil
(ut-Activate 'earth)
earth
(truep '(color-of sky ?y))
((?y . blue) (t . t))~l4269j\1b
Figure 5 - The use of theories in MRS~l4269c\b38B
Stop: The next few sections delve into MRS's meta-description and the ways one can modify it or get MRS to use it in controlling its own operation. This is a fairly complicated discussion and for some applications may be unnecessary, and so the new user is advised to skip the following sections until he has gained some experience with the initial system and encountered the need to make modifications.~j\i2b5B
2.5 Meta-Description~j\i
In MRS knowledge representation is an application domain in its own right, just like geology or medicine. The system contains knowledge about its own structure and behavior and some popular variations. This information is encoded within the MRS formalism itself, and as a result the system can apply to it the same deductive routines that it uses in reasoning about external domains.~j\225f1 1f0
As described above, symbols in MRS are used to designate objects in the applications domain. In order to state facts about a symbol itself, one needs a separate symbol to represent it. In MRS these "metasymbols" are by convention named by prefixing the symbol represented with an ↑. Consider, for example, the symbol bachelors that represents the set of all bachelors and the symbol ↑bachelors that stands for that symbol. Clearly, it is appropriate to add the assertion (mem bachelors set), and certainly it is the case that (not (mem ↑bachelors set)). If bachelors and ↑bachelors were coalesced, a contradiction would result. Similarly, one might have an assertion about the size of a person named John, e.g. (size John large), and a contradictory assertion about the size of the symbol representing John, e.g. (size ↑John small). In MRS a symbol and its metasymbol are connected by the denoted-by relation, e.g. (denoted-by John ↑John).~j\284b1B37b9B57b10B79b19B36b26B6b9B5b10B131b17B85b18B59b10B16b23B
Terms, like symbols, designate objects in the application domain; and, as with symbols, a separate symbol is necessary whenever one wants to state a fact about the term itself. The ↑ convention can be used here as well. For example, the term (color-of clyde) designates a point on the visual spectrum, whereas the symbol ↑(color-of clyde) designates an atom in MRS.~j\184b1B61b16B56i6bI18B
Since propositions don't refer to objects in the application domain, they can be used to designate themselves when used as an argument in another proposition. Figure 6 shows some examples of this in representing dependency and theory information. ~j
(dependency (resistance r1 100) (voltage v1 5))
(MyTheory (president US Kennedy) 1961-1963)~j\b
Figure 6 - Some meta-assertions~c\b33B
In order to talk about propositions, a few special vocabulary items are defined. (Rel p) designates the symbol in the relational position of the proposition; (arg p) designates the symbol in the argument position; and (val p) designates the symbol in the value position. (Prop ↑r ↑a1 . . . ↑an) designates the proposition symbol made up of the indicated symbols, i.e. (r a1 . . . an).~j\84b7B70b7B53b7B47b11o252 1o0 9o252 1o0 1B74b4o252 1o0 8o252 1o0 1B
As examples of the information MRS has about itself, consider the facts shown in figure 7. The first assertion specifies that the subroutine stash is to be used in asserting propositions containing any relation about which no other information is known. MyToAssert is the unary function that connects a relation with the subroutine used to assert it. The second assertion specifies unstash for removing assertions. The third assertion states that the inference methods used by truep is bs-truep, i.e. backward chaining.~j\144b5B109b10B119b7B89b5B4b8B
(if (expression $x) (MyToAssert $x stash))
(if (expression $x) (MyToUnassert $x unstash))
(if (expression $x) (MyToTruep $x bs-truep))~l4269j\b
Figure 7 - Some Facts about how MRS deals with propositions~c\b
2.6 Advice-Taking and Explanation~j\1i
Given MRS's formalism and an adequate meta-level vocabulary, it's possible for a user of MRS to ask questions about the system itself; and, since the system has a partial description of itself, it can answer many of these questions. More importantly, the system uses its own description (as explained below) in carrying out each operation. The upshot is that the user can affect MRS's behavior simply by modifying this description.~j
The exact mechanism for this should be clear after a look at how MRS works. Figure 8 presents the initial LISP definitions of three of MRS's user-level commands. Each calls the subroutine kb with its corresponding MyTo relation and its argument. Kb first uses backward chaining to decide how to carry out the operation and extracts it from the binding list using subvar. It then applies the result to the specified argument. (Kb can be thought of as a general problem solver that achieves the goal of its caller, e.g. (asserted p). The version presented here is fairly trivial, but more interesting versions are possible. This point is elaborated further in section 2.7.)~j\110f1 3f0 79b2B24b4B29b2B115b6B59b2B90b12B143b
(defun assert (p) (kb 'MyToAssert p))
(defun unassert (p) (kb 'MyToUnassert p))
(defun truep (p) (kb 'MyToTruep p))
(defun kb (g x)
(funcall (subvar '? (bs-truep '(g x ?))
x))~jk144\b
Figure 8 - Definitions of MRS's user level subroutines~c\b
As a very simple example, consider how MRS handles a request like (truep '(color-of clyde grey)). A trace of the relevant function calls is shown in figure 9. Truep calls kb with arguments MyToTruep and (color-of clyde grey). Kb uses bs-truep to determine how to look up the proposition and finds bs-truep. It then calls bs-truep to get the answer.~j\68b30B65b5B7b2B16b9B5b21B3b2B6b8B55b8B17b8B19b
(enter truep (color-of clyde grey))
(enter kb MyToTruep (color clyde grey))
(enter bs-truep (MyToTruep (color-of clyde grey) ?))
. . .
(exit bs-truep bs-truep)
(enter bs-truep (color-of clyde grey))
. . .
(exit bs-truep ((t . t)))
(exit kb ((t . t)))
(exit truep ((t . t)))~l4269j\b
Figure 9 - A trace of function calls in answering a request~c\b60B
Since MRS actually uses its description in deciding how to do an operation, changing this description can change its behavior. The following examples show how a user can modify the system in a few popular ways by changing its description.~j
Example - Changing the Inference Algorithm~j\1i42I
Suppose one wanted to convert MRS into a data base system without inference. To do this, the only change that is necessary is to replace the backward chaining prescribed in figure 7 to direct lookup, as shown below. Thereafter, whenever truep is called, kb will find lookup, and no further deduction will be performed.~j\241b5B12b2B11b6B
(unassert '(if (expression $x) (MyToTruep $x bs-truep)))
(assert '(if (expression $x) (MyToTruep $x lookup)))~l4269j\b
Figure 10 - Switching from backward chaining to direct lookup~c\b62B
Example - Changing the Representation~j\1i
While the propositional representation is adequate for representing all types of information, property lists are a good example of a specialized data structure that is especially suited to storing the values of unary functions. For example, the assertion (color-of Clyde grey) can be represented by a color-of property on Clyde's property list. The commands in figure 11 show how property lists can be utilized in MRS. In particular, they name the LISP subroutines for accessing and modifying property lists. Of course, its is necessary to assert that a relation is a unary function (either directly or indirectly) in order for this information to be found.~j\258b21B25b8B13b5B124f1 3f0
(assert '(if (and (rel $p $r) (unaryfun $r)) (MyToStash $r pl-stash)))
(assert '(if (and (rel $p $r) (unaryfun $r)) (MyToUnstash $r pl-unstash)))
(assert '(if (and (rel $p $r) (unaryfun $r)) (MyToLookup $r pl-lookup)))
(defun pl-stash (p) (putprop (cadr p) (caddr p) (car p)))
(defun pl-unstash (p) (remprop (cadr p) (car p)))
(defun pl-lookup (p) (eq (caddr p) (get (cadr p) (car p))))~l4269j\1b
Figure 11 - Storing unary functions on property lists~c\b54B
Example - Procedural Attachment~j\i32I
Procedural attachment is the association of a procedure with a "slot" in a "frame" that is executed whenever a value is added to, needed for, or removed from that slot. In MRS procedural attachment is effected by appropriate MyToAssert, MyToUnassert, and MyToTruep properties on the relation corresponding to the "slot". For example, suppose one wanted to build a kinship data base in which only mother-of and spouse-of links were stored, leaving father-of to be computed. In MRS this could be implemented by placing the appropriate properties on father-of as shown in figure 12. When truep is called with (father-of clyde ?y) as argument, kb finds the truep-father procedure and applies it.~j\228b10B2b12B6b9B133b9B5b9B28b9B91b10B30b5B16b16B1b4B13b2B11b12B
(assert '(MyToTruep father-of truep-father))
(defun truep-father (x)
(truep '(exist y (and (mother-of ,(cadr x) y) (spouse-f y ,(caddr x))))))~l4269j\1b
Figure 12 - Computing the father-of relation~c\b
Of course, this could have been done more generally as shown in figure 13. Father-of is asserted to be a member of the set of ComposedFunctions and is defined as the composition of spouse-of and mother-of. All composed functions have truep-composed as their MyToTruep property. Therefore, when truep is called on (father-of clyde ?y), kb finds truep-composed, which computes the answer as before. The difference here is that, to implement a new composed function, one need only assert that it is a member of ComposedFunctions and indicate the composing functions.~j\78b9B42b17B38b9B5b9B31b14B10b9B28b5B14b20B2b2B7b14B151b17B
(assert '(mem father-of ComposedFunctions))
(assert '(composition* spouse-of mother-of father-of))
(assert '(if (and (rel $x $r) (mem $r ComposedFunctions))
(MyToTruep $r truep-composed))
(defun truep-composed (x)
(prog (dum)
(setq dum (truep '(composition* ?x ?y ,(car x))))
(return (truep (list 'and (list (subvar '?x dum) (cadr x) ?z)
(list (subvar '?y dum) ?z (caddr x)))))))~l4269j\1b
Figure 13 - Implementation of composed functions~c\b49B
Example - Truth Maintenance~j\1i27I
Another example is the partial implementation of truth maintenance. Suppose, for example, that dependency information is stored as suggested in figure 6, i.e. as dependency propositions connecting each assertion to the propositions it depends on. (For simplicity, the possibility of multiple justifications is ignored in this example.) One can define a truth maintenance subroutine UnassertMaintain that removes assertions from the data base whenever their support is removed. The code for UnassertMaintain and the appropriate meta-assertion are shown in figure 14. As a consequence of this assertion, every time Unassert is called, UnassertMaintain will be used and the dependencies will be removed.~j\165b10B212b16B93b16B108b8B12b16B
(assert '(if (expression $x) (MyToUnassert $x UnassertMaintain)))
(defun UnassertMaintain (p)
(unstash p)
(mapc 'unassert (getvals* (list 'dependency p))))~l4269j\b67B1b
Figure 14 - Partial implementation of Truth Maintenance~c\b
2.7 Meta-Control~j\1i
In the very simple examples presented above, the system's meta-level reasoning was based solely on syntactic information about the propositions it was processing. In different versions of the system, this reasoning might be considerably more extensive.~j
Suppose, for example, the user had made the assertions (composition spouse-of mother-of father-of) and (composition spouse-of father-of mother-of). If the procedural attachment approach of section 2.6 were applied with this data base, the system would go into an infinite loop, first trying to find father-of in terms of mother-of, then trying to find mother-of in terms of father-of. One could eliminate this possibility in many common cases by using a more complicated retrieval that first checks whether the indicated method will halt. See figure 15. If MRS can prove that the indicated method does not halt, it can notify the user rather than embarking on the endless computation. This deduction may itself involve the use of bs-truep on the halting problem and might use rules for proving termination like those suggested in [Genesereth] and elsewhere.~j\57b43B5b43B154b9B13b9B22b9B13b9B351b8B
(defun kb (g x)
(prog (f)
(setq f (subvar '? (bs-truep (list g x '?)))
(if (bs-truep '(not (halting f x)))
(print 'Nonhalting)
(return (funcall f x)))))~l4269j\1b
Figure 15 - Meta-reasoning to prevent an infinite loop~c\b
Another example of more substantial meta-reasoning is the choice of one search method over another. Suppose, for example, that one had encoded an ancestor hierarchy and requested MRS to check whether beatrice is an ancestor of clyde. To do this, the system must decide whether to search beatrice's descendants or clyde's ancestors. In making this decision, it could reason that the branching factor in the upward direction is less than the branching factor downwards and, therefore, it's quicker to search upwards.~j\149b8B46b8B19b5B56b8B18b5B
The above two examples have not yet been implemented, but MRS does provide a framework in which they are possible. Meta-control is an important and interesting research area, and the development of these capabilities is a high priority task for the authors.~j
2.8 Complete Modifiability~j\i
As was indicated in the introduction, a unique feature of MRS is that it is intended to be completely modifiable, i.e. it can be converted into any LISP program, purely by assertions within its own formalism. Of course, LISP is similarly modifiable, but MRS will be different in the degree to which it will facilitate the transformation to other interesting behaviors. As with meta-control this capability of the system is not yet finished, but it is under active development. Interested readers should consult [Genesereth & Lenat] for further discussion.~j\151f1 3f0 70f1 3f0
Earlier, it was stressed that MRS permits many different representations for assertions, e.g. property lists, bit vectors, and LISP code. In several of the examples above, the modification included the definition of LISP subroutines. Storing procedures in the form of Lisp code is one of the alternatives to MRS's propositional net, and all completely specified procedures are stored in this format. In this one case, the internal representation is shown, since it is easier to read. (In point of fact, one can easily describe Lisp code as sets of assertions. Each s-expression can be represented as an individual action with an operator, inputs, outputs, and controlflow. This representation is especially useful in defining partial procedures and making small changes in a piece of code.)~j\130f1 3f0 87f1 3f0
This representation of procedures as LISP subroutines is the key to MRS's guarantee of complete modifiability. Since any LISP subroutine can be described as MRS assertions and then executed, MRS will inherit the complete power of LISP (which is completely modifiable). The definitions of MRS's subroutines and its meta-description facilitates many common modifications; but, for users who desire a capability that doesn't fit within this general framework, MRS will make the full power of LISP available.~j\40f1 3f0 82f1 3f0 106f1 3f0 257f1 3f0
In fact, each of the user-level commands in MRS is itself a symbol in the data base, and the user can modify its assertions like those of any other symbol, thereby changing the definitions. Ultimately, MRS will maintain dependency links between each of the assertions describing these subroutines and their LISP definitions; and, if the user changes any of these links, the system will change the code accordingly. ~j\311f1 3f0
3. MRS's Subroutines~j\i
MRS provides its user with several levels of subroutines for accessing and modifying its data base. One important property of the user-level commands is that they are treated as "goals", i.e. the system reasons about how to achieve them, as described in section 2.6.~j
3.1 User Level Subroutines~j\1i27I
Important note: In order to facilitate interaction with MRS, there is an additional sequence of commands that check the user's input for errors and reformat them as necessary. This preprocessing is separated from the basic routines described below so that they can be used in programs without sacrificing the time necessary to perform these error checks and reformatting. The names of these error-checking and reformatting commands are obtained by prefixing the names below with dollar signs ("$"). For example, ($Assert p) removes all prefix quantifiers, records appropriate skolem information, and calls Assert on the result. The commands $Assert*, $Unassert, $Unassert*, $Truep, $Truep*, $Trueps, $Trueps*, etc. are analogously defined. Until one is thoroughly familiar with MRS, one should always use the "$" versions.~j\1b15B481b1B18b11B53b6B24b6B30b8B2b9B2b10B2b6B2b7B2b7B2b8B6b1B26b82B
Currently, the "plural" functions return lists of all appropriate items. In the next version of MRS, these explicit lists may be replaced with generator functions.~j
MRS has two series of commands. Each of the commands in the first series (assert, unassert, truep, etc.) does backward chaining to determine how much inference to perform in handling its argument and then calls the resulting inference method. Each of the commands in the second series (stash, unstash, lookup, . . .) does backward chaining to determine how to represent its argument and then calls the indicated method without inference. ~j\77b6B2b8B2b5B190b5B2b7B2b6B131b
(Assert p) runs the assertion method indicated by p's MyToAssert property. ~j\b11B40b1B3b10B
(Unassert p) runs the deletion method indicated by p's MyToUnassert property. ~j\b13B39b1B3b12B
(Truep p) runs the inference method indicated by p's MyToTruep property.~j\b10B40b1B3b9B
(Trueps p) runs the inference method indicated by p's MyToTrueps property.~j\i1bI10B40b1B3b10B10b
(Getbdg p) is equivalent to (cdar (truep p)), i.e. it assumes p contains exactly one existential variable and returns the value of that variable in the resulting binding list.~j\b11B18b16B18b1B112b
(Getbdgs p) is equivalent to (mapcar 'cdar (trueps p)), i.e. it assumes p contains exactly one existential variable and returns the values of that variable in each of the resulting binding lists.~j\b13B16b26B18b1B122b
(Getval (r x1 . . . xn)) uses the method indicated by its MyToGetval property, which is usually equivalent to (getbdg (r x1 . . . xn ?y)).~j\b25B34b11B41b27B1b
(Getvals (r x1 . . . xn)) uses the method indicated by its MyToGetvals property, which is usually equivalent to (getbdgs (r x1 . . . xn ?y)).~j\b26B34b11B42b28B1i
(Stash p) places assertion p in the data base, using the method indicated by its MyToStash property.~j\i2bI9B18b1B53b9B10b
(Unstash p) removes the assertion p from the data base, using the method indicated by its MyToUnstash property. Note this is not equivalent to asserting the negation of p.~j\b12B23b1B55b11B42b1B26b1B1b
(Lookup p) checks whether the proposition p is asserted in the current data base, using the method indicated by its MyToLookup property. If p contains any existential variables, the result is a list of variable bindings that satisfies p. If p is free of existential variables and p is true, the result is the default binding list ((t . t)).~j\b11B32b1B73b10B15b1B94b1B6b1B38b1B49b9B1b
(Lookups p) checks whether the proposition p is asserted in the current data base, using the method indicated by its MyToLookups property. If p contains any existential variables, the result is a list of binding lists that satisfy p. If p is free of existential variables and p is in the data base, the result is (((t . t))).~j\b13B31b1B73b11B15b1B88b1B6b1B38b1B36b11B1b
(Lookupval (r x1 . . . xn)) uses the method indicated by its MyToLookupval property, which is usually equivalent to (subvar '?y (lookup (r x1 . . . xn ?y))).~j\b28B34b13B42b40B1b
(Lookupvals (r x1 . . . xn)) uses the method indicated by its MyToLookupvals property, which is usually equivalent to (mapcar '(lambda (l) (subvar '?y l)) (lookups (r x1 . . . xn ?y))).~j\b29B34b14B42b67B1i
3.2 Predefined Inference Methods~j\i
(pi-truep p) uses property inheritance to determine whether p is true. For example, if the data base contained the assertions (mem clyde elephants), (subclass elephants mammal), and (if (mem $x mammals) (temperature $x warm)), then (pi-truep (temperature clyde warm)) would return ((t . t)) Currently, this works only in the Interlisp version.~j\b13B48b1B9b1B56b21B2b27B6b43B7b35B14b9B54b
(bc-truep p) uses backward chaining to determine whether p is true.~j\b13B45b1B9b
(bs-truep p) is equivalent to (or (lookup p) (bc-truep p)). For example, if the data base contained the assertions (if (mem $x birds) (flies $x)), (if (feathered $x) (mem $x birds)), and (feathered Herbie), then (bs-truep (flies Herbie)) would return ((t . t)).~j\b13B18b28B1b2B55b30B2b34B6b18B7b25B14b9B1i
3.3 Propositional Representation Subroutines~j\1i
(pr-stash p) adds the proposition p to the data base.~j\1b13B21b1B
(pr-unstash p) removes the proposition p from the data base.~j\1b14B25b1B
(pr-lookup p) checks whether the proposition p is in the data base and, if so, returns the proposition symbol.~j\1b13B32b1B
(ex-lookup p) uses a matching procedure to determine whether p is implied by the data base. It matches universal variables in the data base and existential variables in p only. For example, the data base assertion (r $x $x $y d) matches the pattern (r a a (f ?z) ?z) with the result (($x . a) ($y . (f ?z)) (?z . d)).~j\b14B48b1B108b1B45b14B21b17B17b33B1b
(pr-lookupval (f a)) checks whether there is a proposition of the form (f a b) in the data base and, if so, returns b.~j\1b20B51b7B38b1B
(pr-lookupvals (f a)) is similar to pr-lookupval except that it returns a list of all objects b satisfying (f a b).~j\1b21B15b12B46b2B11b7B
CurrentTheory is the name of the currently writeable theory. Any atom is an acceptable theory name.~j\1b14B
ActiveTheories is a list of all the currently active theories, those whose assertions are available for retrieval or deduction.
(ut-NewTheory c1 . . . cn) generates a garbage-collectible theory with subtheories c1 . . . cn. Currently, this works only in the Maclisp version.
(ut-Activate c1 . . . cn) makes the assertions in the theories c1 . . . cn available for access.~j\1b14B115b15o252 1o0 8o252 1o0 1B57b1o252 1o0 8o252 1o0B55b14o252 1o0 8o252 1o0 1B38b1o252 1o0 8o252 3o0B
(ut-Deactivate c1 . . . cn) deactivates the named theories.~j\1b16o252 1o0 8o252 1o0 1B
(ut-Kill c) unasserts all the facts in the theory c.~j\1b11B39b1B
3.4 Data Structure Subroutines~j\2i
(ua-pattern p) returns the pattern corresponding to the proposition symbol p.~j\1b14B61b1B
(ua-datum l) returns the proposition symbol corresponding to the list l.~j\1b12B58b1B
(ua-getfacts n) returns a list of all proposition nodes indexed on n.~j\1b15B52b1B
(ua-list t) returns a list of all symbols that occur in currently asserted propositions. ~j\1b11B
4. The Syntax of MRS~j\1i20I
MRS allows one to enter proposition in the predicate calculus of arbitrary order as well as meta-level assertions. The syntactic rules are described in this section.~j
First-Order Propositions in MRS~j\1i
There are two types of symbols in MRS, viz. variables and constants. Variables are useful for stating facts about all members of a set or for declaring the existence of an object without naming it. The use of variables is elaborated below in the discussion of quantified propositions.~j\46i9I5i9I
There are three different types of constant symbols. Object symbols name specific objects or concepts in the world being described, e.g. Stanford, Kennedy, elephants (the set thereof), blue, and justice. Function symbols are intended to represent functions on the objects of the world, e.g. president-of, height-of, cardinality-of, sin, +, *, and color-of. Relation symbols represent relations between objects of the world, e.g. neighbor, subclass, >, =, and older-than.~j\56i14I70b8B2b7B2b9B20b4B6b7B3i16I71b12B2b9B2b14B2b3B2b1B2b1B6b8B3i16I56b8B2b8B2b1B2b1B6b10B
In MRS one can also designate objects by combining these symbols into more complex expressions, called terms. All variables and constants are terms by definition. In addition, given an n-ary function symbol f and n terms t1, . . ., tn, then the expression (f t1 . . . tn) is also a term. For example, the following expressions are legal terms: (president-of Stanford), (cardinality-of elephants), (+ 2 2), (height-of (president-of Stanford)), and (* (+ 2 2) 3).~j\105i6I100b1B13b2B9b2B22b15B74b23B2b26B2b7B2b35B6b13B
Facts can be stated withn MRS in the form of propositions. Given an n-ary relation symbol r and n terms t1, . . . , tn, the expression (r t1 . . . tn) is an atomic proposition, e.g. (neighbor Palo-Alto Menlo-Park), (subclass elephants mammals), and (> (* 2 3) (+ 2 3)).~j\47i14I32b1B13b2B2b6B2b2B17b15B7i18I7b31B2b28B6b19B
Unfortunately, not all facts are so simple. One often needs to express negations (e.g. "Lyman is not the president of Stanford), disjunctions (e.g. "Either Lyman is president or Kennedy is president"), and contingencies (e.g. "If George is at home, he must be sick"). In MRS facts like these can be written by relating the appropriate atomic propositions via logical symbols such as not, and, or, and if. For example, these sentences could be written as follows: (not (= (president-of Stanford) Lyman)), (or (= (president-of Stanford) Lyman) (= (president-of Stanford) Kennedy)), and (if (location george home) (sick george)).~j\363i16I9b3B2b3B2b2B6b2B61b39B2b74B6b41B
Finally, there are quantified propositions. With the syntax given so far, one can only write facts by naming the objects involved. There's no simple way to talk about all the members of a set or state the existence of an object without naming it. Quantifiers enable one to state facts like "All apples are red" and "There's a doctor in the house". There are two quantifiers in MRS, viz. all and exist. The proposition (all x1 . . . xn (p x1 . . . xn)) states that (p x1 . . . xn) is true for all possible values of the variable symbols x1, . . . , xn. The proposition (exist x1 . . . xn (p x1 . . . xn)) states that there exist objects a1, . . . , an for which (p a1 . . . an) is true. For example, one can say that all apples are red with the proposition (all x (if (mem x apples) (color-of x red))), and one can say that there's a doctor in the house with the proposition (exist x (and (mem x doctors) (location-of x house))). Quantified propositions can occur within non-atomic propositions, e.g. (or (all x (if (mem x apples) (color-of x red))) (exist x (and (mem x apples) (color-of x green)))) and (all x (exist y (> y x))).~j\393b3B5b5B19b33B13b15B57b2B2b6B2b2B19b35B33b2B10b2B11b15B81b44B74b53B74b99B5b25B
Multiple variables of the same type can be declared within a single quantified proposition, e.g. (all h r (if (and (horse h) (rabbit r)) (can-outrun h r))) and (exist x y (and (= (+ x 1) y) (= (* 2 x) y))). Note, however, that the ordering of quantifiers is essential whenever a quantified proposition is nested within another. For example, the propositions (all x (exist y (loves x y))) and (exist y (all x (loves x y))) mean two very different things. Information about the order of nesting of quantified propositions is sometimes referred to as skolem information.~j\99b58B5b45B155b30B4b29B128i
Higher-Order Propositions~j\1i
In the language described above, function and relation symbols were permitted to occur only in the functional or relational position of terms and propositions, and there was no mention of function or relation variables. The upshot of this is that the terms of the language could only refer to objects and not to functions or relations. This type of language is called a first-order language and is important because there are strong theorems about what and and cannot be proved from propositions in such a language.~j\i1I373i20I
However, it's often useful to state facts about functions and relations as though they were objects and to quantify over functions and relations. In MRS this is perfectly legal. For example, one can state that > is transtive with the proposition (transitive >), and one can state that all equivalence relations are transitive with the proposition (all r (if (equivalence r) (transitive r))). Using higher order quantification, it is also possible to state axioms like the induction principle. For example, the following proposition states that if a relation r is true of 0 and whenever r is true of an integer n it is also true of n+1, then it is true of every integer. ~j\215b1B35b14B87b43B170b1B12b1B14b1B
(all r (if (and (r 0) (all x (if (r x) (r (+ x 1)))))
(all x (r x)))~j\1b
Meta-Propositions~j\b1Bi
Statements about MRS itself can be made in the syntax described above, except using symbols in a different vocabulary, as explained in section 2.4. ~j\i2I147b
5. Vocabulary~j\1i
This section contains a vocabulary of useful terms for encoding information about logic, sets and mappings, arithmetic, and events and time. Most of the terms are mentioned in one or more of the assertions in the appendices or section 6 or are used by one or more of the inference procedures in section 3. A few of the terms are not known to MRS at all and are listed here as suggestions. These terms occur in several programs that use MRS and may someday become part of the initial system.~j\i1I494i
In creating new names, MRS users often observe the following conventions. Sets are usually named in the plural, e.g. resistors is the set of all resistors. Functions that apply to an arbitrary number of arguments are terminated with the symbol *, e.g. (union* s1 s2 s3 s) states that s the union of the sets s1, s2, and s3. ~j\i2I118b9B119b1B7b9o252 1o0 2o252 1o0 2o252 1o0 3B13b2B22b1o252 1o0B1b2o252 1o0B5b2o252 1o0B2i
5.1 Logic~j\i
(= a b) means that the symbols a and b are synonymous, i.e. they refer to the same object.~j\1b7B24b1B5b1B
(Not p) means that the proposition p is false.~j\1b7B28b1B10b
(And p1 . . . pn) means that the assertions p1 . . . pn are all true.~j\b7o252 1o0 8o252 1o0 1B27b1o252 1o0 8o252 1o0B14b
(Or p1 . . . pn) means that one or more of the assertions p1 . . . pn is true.~j\b6o252 1o0 8o252 1o0 1B42b1o252 1o0 8o252 1o0B9b
(Xor p1 . . . pn) means that exactly one of the assertions p1 . . . pn is true.~j\b7o252 1o0 8o252 1o0 1B42b1o252 1o0 8o252 1o0B9b
(If p q) means that whenever proposition p is true, proposition q is true.~j\b9B33b1B21b2B
(Iff p q) is equivalent to (and (if p q) (if q p)).
(All x p) means that p is true for all bindings of the variable x.~j\1b9B18b23B1b11B12b1B42b1B1b
(Exists x p) means that there is some binding for the variable x that makes p true.~j\b13B51b1B12b1B6i
5.2 Sets and Mappings~j\i
Empty is the empty set.~j\1b5B
(Set* a1 . . . an) is the set consisting of the members a1 . . . an.~j\1b7o252 1o0 8o252 1o0 1B38b1o252 1o0 8o252 1o0B
(mem a s) means that a is a member of the set s.~j\1b9B12b1B24b1B
(subclass a b) means that the set a is a subset of the set b.~j\1b15B19b1B24b1B
(union* s1 . . . sn) stands for s1 U . . . U sn.~j\1b9o252 1o0 8o252 1o0 1B12b2o252 1o0 1f3B1f0b7f3B1f0b2o252 1o0B1i
(inter* s1 . . . sn) stands for s1 y . . . y sn.~j\i1bI9o252 1o0 8o252 1o0 1B11b2o252 1o0 1f3B1f0b7f3B1f0b2o252 1o0B1b
(composition* f1 . . . fn) means the unary function composed of the unary functions f1 . . . fn. For example, (composition* spouse mother).~j\b16o252 1o0 8o252 1o0 2B57b1o252 1o0 8o252 1o0B1b2B13b28B1b
(inverse f) is the inverse function of f..~j\1b11B28b1B
(unionf* f1 . . . fn) is the functional union of the functions specified.~j\b11o252 1o0 8o252 1o0 1B52b
(interf* f1 . . . fn) is the functional intersection of the functions specified.~j\b11o252 1o0 8o252 1o0 1B59b
5.3 Arithmetic~j\i
(+ a1 . . . an)~j\i1bI4o252 1o0B1b7o252 1o0
(- a b)~j\b
(* a1 . . . an)~j\b5o252 1o0B1b7o252 1o0
(> a b)~j\b
~j\b
(>= a b)~j\b
(<= a b)~j\b
(< a b)~j\b8Bi
5.4 Events and Time~j\i
Events in MRS are viewed as individual occurrences of actions.~j\i2I
(act r rplacd) means that the event r is an occurrence of the rplacd action.~j\1b14B22b1B25b6B
(input* r a1 . . . an) means that the event r has inputs a1 . . . an.~j\1b11o252 1o0 8o252 1o0 1B22b1B12b1o252 1o0 8o252 1o0B1i
(output* r a1 . . . an) means that the event r has outputs a1 . . . an.~j\1b12o252 1o0 8o252 1o0 1B22b1B13b1o252 1o0 8o252 1o0B
(true p s) means that the assertion p is true in the situation s. This is useful in describing the behavior of synchronous worlds. For example, one can describe the behavior of an inverter (in which the output out at one instant is the opposite of the input in at the preceding instant) with the assertion (if (true (on in) $s) (true (off out) (succ $s))).~j\i1bI10B26b1B26b1B148b4B44b3B45b49B
(happens a s) means that the action a is initiated in situation s. For example, (if (true (buffer-contains $x) $s)) (exists (p) (and (act p print) (input* p $x) (happens p $s)))) says that whenever a character appears in a buffer, it gets printed. Happens is useful in describing the behavior of asynchronous systems.~j\1b13B23b1B27b1B16b100B70b7B
(do* a1 . . . an s) returns the situation that results from simultaneously performing the actions a1 . . . an in situation s. For example, (if (and (act $r rplacd) (input* $r $a $c)) (true (cdr $a $c) (do* $r $s))).. Do is useful in describing the behavior of asynchronous systems.~j\1b6o252 1o0 8o252 1o0 3B79b1o252 1o0 8o252 1o0B14b1B16b75B4b2B62i
5.5 Meta-Level Vocabulary~j\i
(MyToAssert p f) means that the subroutine f is to be called in asserting the proposition p. Each of MRS's user-level commands has associated with it a relation that specifies the subroutine to be used in carrying out that command. The relation is named by prefixing the command's name with MyTo, e.g. MyToAssert. There are similar relations for each of the commands in section 3.1.~j\1b16B28b1B46b1B202b4B7b10B
(Rel p) is the symbol in the relational position of the proposition p.~j\1b7B61b1B
(Arg p) is the symbol in the argument position of the proposition p.~j\1b7B59b1B
(Val p) is the symbol in the value position of the proposition p, i.e. the second argument.~j\1b8B55b1B
(Prop r a1 . . . an) is the proposition symbol made up of the symbols specified. ~j\1b9o252 1o0 8o252 1o0 1B61b
6. Initial Data Base~j\i
6.1 Definitions of the User-level Subroutines~j\i
The Maclisp definitions of the key user-level subroutines in MRS are as follows. The Interlisp versions are equivalent.~j\122b
(defun assert (p) (kb 'MyToAssert p))
(defun unassert (p) (kb 'MyToUnassert p))
(defun truep (p) (kb 'MyToTruep p))
(defun trueps (p) (kb 'MyToTrueps p))
(defun getval (x) (kb 'MyToGetval x))
(defun getvals (x) (kb 'MyToGetvals x))
(defun stash (p) (kb 'MyToStash p))
(defun unstash (p) (kb 'MyToUnstash p))
(defun lookup (p) (kb 'MyToLookup p))
(defun lookups (p) (kb 'MyToLookups p))
(defun lookupval (x) (kb 'MyToLookupval x))
(defun lookupvals (x) (kb 'MyToLookupvals x))
(defun kb (g x)
(let ((goals goals))
(if (memsamep (setq g (list g x '?)) goals) nil
(funcall (subvar '? (or (ex-lookup g) (bc-truep g)))
x))))~l4269j\b
Note that the definition of kb here differs slightly from that presented in section 2. The version of kb in the system first checks the list goals to see whether the goal has occurred before and, if so, halts. The point of this check is to prevent infinite recursions when in the process of satisfying a goal, an identical subgoal is generated.~j\30b2B73b2B
6.2 Initial Meta-assertions~j\i
(if (expression $x) (MyToAssert $x stash))
(if (expression $x) (MyToUnassert $x unstash))
(if (expression $x) (MyToTruep $x bs-truep))
(if (expression $x) (MyToTrueps $x bs-trueps))
(if (expression $x) (MyToGetval $x truep-getval))
(if (expression $x) (MyToGetvals $x trueps-getvals))~l4269j\b
~l4269j\b
(if (expression $x) (MyToStash $x pr-stash))
(if (expression $x) (MyToUnstash $x pr-unstash))
(if (expression $x) (MyToLookup $x ex-lookup))~l4269j\b
(if (expression $x) (MyToLookups $x ex-lookups))
(if (expression $x) (MyToLookupval $x lookup-lookupval))
(if (expression $x) (MyToLookupvals $x lookups-lookupvals))~l4269j\b
(MyToTruep (expression $x) lookup)
(MyToLookup (expression $x) tfun) where (defun tfun (x) (listp (cadr x)))
(MyToLookups (if $x $y) ex-lookups)~l4269j\b70B5b
(MyToTruep (rel $p $f) lookup)
(MyToTruep (arg $p $f) lookup)
(MyToTruep (val $p $f) lookup)
(MyToTrueps (rel $p $f) lookups)
(MyToTrueps (arg $p $f) lookups)
(MyToTrueps (val $p $f) lookups)
(MyToLookup (rel $p $f) lookup-rel)
(MyToLookup (arg $p $f) lookup-arg)
(MyToLookup (val $p $f) lookup-val)
(MyToLookups (rel $p $f) lookups-rel)
(MyToLookups (arg $p $f) lookups-arg)
(MyToLookups (val $p $f) lookups-val)
(MyToLookupval (rel $p $f) car)
(MyToLookupval (arg $p $f) cadr)
(MyToLookupval (val $p $f) caddr)~l4269j\b513B
In addition the following assertions are made for purposes of efficiency.~j\75b
(MyToTruep (MyToAssert $p $f) bs-truep)
(MyToTruep (MyToUnassert $p $f) bs-truep)
(MyToTruep (MyToTruep $p $f) bs-truep)
(MyToTruep (MyToTrueps $p $f) bs-truep)
(MyToTruep (MyToStash $p $f) bs-truep)
(MyToTruep (MyToUnstash $p $f) bs-truep)
(MyToTruep (MyToLookup $p $f) bs-truep)
(MyToTruep (MyToLookups $p $f) bs-truep) ~l4269j\b
7. Using MRS~j\i
Copies of MRS and its documentation can be obtained by writing to the Heuristic Programming Project at the following address.~j\i1I
Secretary
Heuristic Programming Project
Computer Science Department
Stanford University
Stanford, California 94305~j
Bugs and comments should be sent either to the above address or via Arpanet to CSD.Genesereth@Score or CSD.Smith@Score.~j\120i
7.1 System Utilities~j\i
($facts n) prints out all assertions about n in the currently active theories. This works only in Maclisp~j\bi1I10i1BI32b1B62bi
(ua-List t) returns a list of all symbols that occur in currently asserted facts.
(Edit n) invokes the LISP editor to permit the user to edit the assertions associated with n. This works in the Interlisp version only.~j\bi1I11B70bi2I8B14f1 3f0 66b1B1i1I42bi
7.2 MRS in Maclisp~j\1i
MRS is defined as a set of subroutines and data structures that can be loaded into any Maclisp program with the load command. On the Score machine, this can be done by typing the following line to any Maclisp program.~j\i2I112b4B102i
(load '|<CSD.MRS>MRS.fasload|)~l4269j\b
7.3 MRS in Interlisp~\i
On Score, MRS is also available in Interlisp as a sysout. It can be obtained by typing the following line to the monitor.~\i1I123i
<CSD.MRS>MRS.exe~l4269\bi1I16i
References~ck792\i
Genesereth, M. R.: "Metaphors and Models", Proc. of the First Annual Conference on Artificial Intelligence, August 1980.~j\f1
Genesereth, M. R. & Lenat, D. B.: "A Modifiable Representation System", HPP-80-26, Stanford University Computer Science Department, Dec. 1980.~j\f1
Greiner, R.: "A Representation Language Language", HPP-80-9, Stanford University Computer Science Department, May 1980.~j\f1
Smith, D. E.: "CORLL: A Storage and File Management System for Knowledge Bases, HPP-80-8, Stanford University Computer Science Department, April 1980.~j\f1